Section: New Results

Integration of formal methods in programming languages

Multi-focus strategies

Participants : Jean-Christophe Bach, Christophe Calvès, Horatiu Cirstea, Pierre-Etienne Moreau.

Like most rewriting engines, Tom patterns combined with traversal strategies, gives the possibility to match and rewrite at any position in a given term. We have extended this classical approach with multi-focus strategies which enable us to match and rewrite several positions simultaneously. More precisely, the action performed at a given position can depend on the other positions involved in the corresponding strategy. This extension is particularly well-suited for programming-language semantics specification, semantics which usually require gathering several subterms (code, memory, input/output channels, ...) to perform one action.

The multi-focus library is a conservative extension of Tom standard strategies and provides combinators to handle multi-position traversal, matching and rewriting. Compared to the original Tom strategy library, the multi-focus version provides global backtracking. The library is available at http://gforge.inria.fr/projects/tom .

Formal islands grammars parsing

Participants : Jean-Christophe Bach, Pierre-Etienne Moreau.

Extending a language by embedding within it another language presents significant parsing challenges, especially if the embedding is recursive. The composite grammar is likely to be nondeterministic as a result of tokens that are valid in both the host and the embedded language. In [9] , we examined the challenges of embedding the Tom language into a variety of general-purpose high level languages. The current parser of Tom is complex and difficult to maintain. In this paper, we described how Tom can be parsed using island grammars implemented with the Generalised LL (GLL) parsing algorithm. The grammar is, as might be expected, ambiguous. Extracting the correct derivation relies on a disambiguation strategy which is based on pattern matching within the parse forest. We described different classes of ambiguity and proposed patterns to solve them.